PRISM
=====
Version: 4.5.dev
Date: Sat Apr 03 03:14:48 CEST 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 pnueli-zuck.30.prism pnueli-zuck.props --property live
Parsing model file "pnueli-zuck.30.prism"...
Type: MDP
Modules: process0 process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15 process16 process17 process18 process19 process20 process21 process22 process23 process24 process25 process26 process27 process28 process29
Variables: p0 p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22 p23 p24 p25 p26 p27 p28 p29
Parsing properties file "pnueli-zuck.props"...
1 property:
(1) "live": Pmax=? [ F (p1=10) ]
---------------------------------------------------------------------
Model checking: "live": Pmax=? [ F (p1=10) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 213 iterations in 41.76 seconds (average 0.196056, setup 0.00)
Time for model construction: 43.47 seconds.
Type: MDP
States: 1.8999999999982707E31 (1 initial)
Transitions: 7.3559999999923E32
Choices: 6.803999999992932E32
Transition matrix: 199786 nodes (3 terminal), 7.3559999999923E32 minterms, vars: 120r/120c/30nd
Warning: Switching to MTBDD engine, as number of states is too large for Sparse engine.
Prob0A: 270 iterations in 1531.93 seconds (average 5.673807, setup 0.00)
----------
Computation aborted after 1800.0933043956757 seconds since the total time limit of 1800 seconds was exceeded.